COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	PROC1(M B)
C00003 00003	CLIMBING FRAME ITERATION RULE:
C00004 ENDMK
C⊗;
PROC1(M B)
BEGIN
 TRAVEL(M P CORNER)
 IF ¬UNDER(SHOES CHAIR2 CORNER) THEN
	PROC2(M SHOES CORNER)
 ELSE
	BEGIN
	FIND(M SHOES CORNER);
	END
 REACH(M SHOES CORNER);
 PUT_ON(M SHOES);
 TRAVEL(M CORNER SLOC);
 MOVE(M B12 SLOC U);
 CLIMB(M B12 U);
 Y4 ← B21;
 WHILE ¬STACKEDN((4) U) DO
	BEGIN
	Y1 ← Y4;
	WHILE STACKED (Y1 Y2 U) DO
	 UNCLIMB(M Y1 U);
	TRAVEL(M U SLOC)
	NEXTBOX(Z4 Y4);
	MOVE(M Z4 SLOC U);
	LIFT(M Z4 U);
	Y1 ← B12;
	WHILE STACKED (Y2 Y1 U) DO
	 CLIMB(M Y2 U);
	STACK(M Z4 U);
	Y4 ← Y1;
	END;
 CLIMB(M Y1 U);
 REACH(M B U);
END

CLIMBING FRAME ITERATION RULE:

BASIS: ROBOT(M) ∧ ON(M X1);
INVARIANT: ON(M X1);
ITERATION STEP GOAL: ON(M X2);
CONTROL TEST: STACKED(X2 X1);
GOAL: ONTOP(M);


OUTPUT:
Y1 ← B1;
   WHILE STACKED(Y2 Y1) DO CLIMB (M Y1 Y2);

Q∧L{?}R∨¬L GIVES:
ON(M,X1)∧STACKED(X2 X1) {?} ON(M X2) ∨¬STACKED(X2 X1)